HECTOR在算法模块形式化数据通路验证中的应用
📑 目录
- 1. 
- 2. 
- 3. 
- 4. 
- 5. 
- 6. 
- 7. 
- 8. 
- 9. 
- 10. 
- 11. 
- 12. 
- 13. 
- 14. 
- 15. 
- 16. 
- 17. 
- 18. 
- 19. 
- 20. 
- 21. 
- 22. 
- 23. 
- 24. 
HECTOR在算法模块形式化数据通路验证中的应用
作者: Yu Zhishuai (HUAWEI TECHNOLOGIES CO., LTD)
会议: SNUG China 2018
页数: 24
源文件: SNUG_CN_Dorso_Untitled_paper_7.pdf
Page 1
HECTOR在算法模块形式化数据通路验证中的应用
Yu Zhishuai HUAWEI TECHNOLOGIES CO., LTD 2018/6/4, China
Page 2
议程 - 背景 - HECTOR介绍 - 典型应用场景 - 相关统计数据 - 总结与建议
Page 3
背景 — 算法运算的特征 - 密集型计算，并行计算 - 算法函数，矩阵运算 - 浮点/定点计算 - 对精度和速度的高要求
Page 4
算法验证的挑战 — 规模 芯片的规模在不断增长，但验证周期有限，验证工程师的数量不会以芯片规模增长的速度增长。
Page 5
算法验证的挑战 — 验证空间 - 不可能遍历所有可能的输入 - 构建覆盖率模型和运行数千个测试用例需要大量时间
Page 6
算法验证的挑战 — 过多的监控器 - 大量内部节点需要监控，以发现可能在输出端观察不到的内部错误 - 这些大量监控器增加了验证工程师的工作量
Page 7
算法验证的挑战 - 算法仿真效率低 - 很难通过仿真100%证明算法模块 - 只有有限的信号可以与参考模型进行比较 - 难以从DUT和RM的不一致性中定位RTL错误 - 算法模块验证过程中调试时间过长
Page 8
等价性检查的多种应用 - 事务等价性（HECTOR）：比较事务结束时的输出，假设输入相等 - 时序等价性（VC Formal SEQ）：比较每个周期的输出，假设输入和起始状态相等 - 布尔等价性（Formality）：匹配比较点，比较布尔扇入逻辑
Page 9
HECTOR介绍 - 证明独立开发模型的一致性 - 穷举验证连续设计改进 - 不需要测试平台、断言或覆盖率
Page 10
HECTOR介绍（续） - 应用领域：块级、数据通路、事务等价性和属性检查 - 事务长度必须是有界的（几十个周期可以，数百个或更多效果不佳）。组合设计可以 - 如果事务相对独立，HECTOR最容易使用 - 事务间保留大量状态会增加设置复杂性 - 容量取决于内部等价性和/或可识别的设计结构 - 主要商业应用：FPU和算法函数
Page 11
HECTOR介绍 — C/C++要求 - 编译时每个循环的最大迭代次数必须已知 - 最大递归深度必须已知 - 有限使用动态内存分配（new, delete） - 不支持的功能：预编译库不能被引用 - 所有源代码必须由HECTOR编译
Page 12
验证方法 - C++/C模型与RTL之间通过HECTOR进行一致性检查 - 仿真和HECTOR是互补的
Page 13
典型应用场景 — 浮点(fp32)乘加运算
X * X + X * X + ... + add
Page 14
典型应用场景 — 浮点(fp32)乘加运算
| 属性 | 详情 |
| 模块 | 浮点乘法和加法 |
| 特征 | FP32计算，包括乘、加、减、截断操作等 |
| 验证空间 | 无限验证空间，仿真不能覆盖所有输入组合场景 |
| RTL代码行数 | < 1000 |
| C/C++代码行数 | < 500 |
| HECTOR验证时间 | < 1天（HECTOR运行3小时） |
| HECTOR优势 | 更快的收敛速度，验证空间完整 |
| 发现Bug数 | 2 |
Page 15
典型应用场景 — 多级乘法
| 属性 | 详情 |
| 模块 | 多级乘法 |
| 特征 | 定点计算，包括乘、加、移位、舍入等 |
| RTL代码行数 | < 1000 |
| C/C++代码行数 | < 500 |
| HECTOR验证时间 | < 1天（HECTOR运行20小时） |
| HECTOR优势 | 计算链路长，HECTOR可遍历所有边界情况 |
| 待改进 | 运行时间长，级数越多操作耗时越多 |
| 发现Bug数 | 1 |
Page 16
典型应用场景 — 移位操作
（图示：多个移位、交叉开关、加法混合操作的数据通路）
Page 17
典型应用场景 — 移位操作
| 属性 | 详情 |
| 模块 | 移位操作 |
| 特征 | 超过8个输入，不同数据宽度；多个MUX、截位、移位和加法混合；多个流水级 |
| RTL代码行数 | < 500 |
| C/C++代码行数 | < 200 |
| HECTOR验证时间 | < 1天（运行40分钟） |
| HECTOR优势 | 不需要大量随机用例即可快速证明；减少人力和机器资源 |
| 发现Bug数 | 2 |
Page 18
典型应用场景 — 查找表
| 属性 | 详情 |
| 模块 | 查找表 |
| 特征 | 大规模查找表，输入复杂 |
| RTL代码行数 | < 24000 |
| C/C++代码行数 | < 1000 |
| HECTOR验证时间 | < 1天（编译时间长，运行时间短） |
| HECTOR优势 | 可遍历所有输入，效率更高 |
| 待改进 | 编译时间长，最大规模有限 |
| 发现Bug数 | 1 |
Page 19
相关统计数据 — HECTOR在算法验证中的统计
| 指标 | 数据 |
| 用户数 | 5 |
| HECTOR使用的模块数 | > 50 |
| RTL代码行数 | > 30,000 |
| C++/C模型代码行数 | > 7,000 |
| HECTOR发现的总Bug数 | > 50 |
| 效率提升(Bug发现) | > 50% |
| 效率提升(算法证明) | >> 100% |
Page 20
相关统计数据 — HECTOR与其他工具对比
| 模块 | HECTOR | 其他工具 |
| FP32 乘加 | < 3小时(证明) | 20天(不完整) |
| 多级乘法 | < 20小时(证明) | 10天(不完整) |
| FP33_mult | < 10分钟(证明) | Error(规模太大) |
Page 21
总结与建议 — 优势 - HECTOR环境易于搭建 - 约束容易添加 - 验证空间完整 - 在验证算法模块方面效率更高，更少的工序和时间 - Bug发现和定位效率高 - 与仿真互补
Page 22
总结与建议 — 待提升 - C++/C模型需要为HECTOR进行调整 - 对控制逻辑的支持不友好 - 对模块规模有严格要求，适合模块级（不适合BT/IT/ST） - 无法实现精确的覆盖率统计 - 完全证明判断的准确性有待提高
Page 23
总结与建议 - 在验证算法模块方面高效，用于检查RTL与C/C++/SystemC的一致性 - 计算模块的完整性保证 - 效率提升明显 - 需要更多专用求解器
Page 24
谢谢！Thank You
图片索引
本文共 138 张图片，存放于 SNUG_CN_Dorso_Untitled_paper_7_images/ 目录。